Inference at * 1 2 
Iof proof for Lemma decidable implies better:

.....wf..... NILNIL

1. P : 
2. Q : x:P.
3. Dec(P)
  (P  Dec(Q))   

latex

 by  Auto 

latex

 1: .....unproved Inclusion subgoal..... NILNIL

 1: 4. P
 1:   Q  Type
 .

Definitions	P  Q, Dec(P), x:A. B(x), , t  T
Lemmas	decidable wf